home *** CD-ROM | disk | FTP | other *** search
/ Garbo / Garbo.cdr / mac / progrmng / cmlmcmpw.sit / Caml Light / examples / kb / order.ml < prev    next >
Encoding:
Text File  |  1991-05-23  |  2.6 KB  |  78 lines  |  [TEXT/MPS ]
  1. (*********************** Recursive Path Ordering ****************************)
  2.  
  3. #open "prelude";;
  4. #open "terms";;
  5.  
  6. type ordering = Greater | Equal | NotGE;;
  7.  
  8. let ge_ord order pair = match order pair with NotGE -> false | _ -> true
  9. and gt_ord order pair = match order pair with Greater -> true | _ -> false
  10. and eq_ord order pair = match order pair with Equal -> true | _ -> false
  11. ;;
  12.  
  13. let rem_eq equiv = remrec where rec remrec x = function
  14.      []  -> failwith "rem_eq"
  15.   | y::l -> if equiv (x,y) then l else y :: remrec x l
  16. ;;
  17.  
  18. let diff_eq equiv (x,y) =
  19.   let rec diffrec = function
  20.       ([],_) as p -> p
  21.     | (h::t, y)   -> try diffrec (t,rem_eq equiv h y)
  22.                      with failure _ ->
  23.                        let (x',y') = diffrec (t,y) in (h::x',y') in
  24.   if length x > length y then diffrec(y,x) else diffrec(x,y)
  25. ;;
  26.  
  27. (* multiset extension of order *)
  28. let mult_ext order = function
  29.     Term(_,sons1), Term(_,sons2) ->
  30.       (match diff_eq (eq_ord order) (sons1,sons2) with
  31.            ([],[]) -> Equal
  32.          | (l1,l2) ->
  33.               if for_all (fun N -> exists (fun M -> order (M,N) = Greater) l1) l2
  34.               then Greater else NotGE)
  35.   | _ -> failwith "mult_ext"
  36. ;;
  37.  
  38. (* lexicographic extension of order *)
  39. let lex_ext order = function
  40.     (Term(_,sons1) as M), (Term(_,sons2) as N) ->
  41.       let rec lexrec = function
  42.         ([] , []) -> Equal
  43.       | ([] , _ ) -> NotGE
  44.       | ( _ , []) -> Greater
  45.       | (x1::l1, x2::l2) ->
  46.           match order (x1,x2) with
  47.             Greater -> if for_all (fun N' -> gt_ord order (M,N')) l2 
  48.                        then Greater else NotGE
  49.           | Equal -> lexrec (l1,l2)
  50.           | NotGE -> if exists (fun M' -> ge_ord order (M',N)) l1 
  51.                      then Greater else NotGE in
  52.       lexrec (sons1, sons2)
  53.   | _ -> failwith "lex_ext"
  54. ;;
  55.  
  56. (* recursive path ordering *)
  57. (* rpo : (string -> string -> ordering) -> (string -> extension) -> term_pair -> ordering *)
  58. let rpo op_order ext = rporec
  59.   where rec rporec (M,N) =
  60.     if M=N then Equal else 
  61.       match M with
  62.           Var m -> NotGE
  63.         | Term(op1,sons1) ->
  64.             match N with
  65.                 Var n ->
  66.                   if occurs n M then Greater else NotGE
  67.               | Term(op2,sons2) ->
  68.                   match (op_order op1 op2) with
  69.                       Greater ->
  70.                         if for_all (fun N' -> gt_ord rporec (M,N')) sons2
  71.                         then Greater else NotGE
  72.                     | Equal ->
  73.                         ext rporec (M,N)
  74.                     | NotGE ->
  75.                         if exists (fun M' -> ge_ord rporec (M',N)) sons1
  76.                         then Greater else NotGE
  77. ;;
  78.